Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

extract_fa: Fix xor3/xnor3 inversion bug #4691

Merged
merged 2 commits into from
Feb 6, 2025

Conversation

hovind
Copy link
Contributor

@hovind hovind commented Oct 30, 2024

What are the reasons/motivation for this change?

The extract_fa pass seems to have issues when an odd number of inputs are inverted, this is previously reported in #3879 and #4573.

I think @eddiehung solved this in the xor2/xnor2 case in #1297, but the xor3/xnor3 case lacks the equivalent logic.

Explain how this is achieved.

Similarly to how it is handled in the xor2/xnor2 case, we invert the xor3/xnor3 output if the majority3 has an odd number of inverted inputs.

If applicable, please suggest to reviewers how they can test the change.

I have tried to make this break using @jix's test case from #3882.

I don't have much confidence in my understanding of this code, and I hope that some discussion here will help clarify some things for me.

9421558 should perhaps be in a separate pull request (or probably just deleted). I left it in so I could ask if somebody could help clarify to me what the deleted code segment achieves.

84d0c8f I thought initially this was a bug fix, but I'm not sure invert_xy and f2i.inv_a ^ f2i.inv_b can be true at the same time?

Thanks for the amazing tool!

@hovind hovind force-pushed the experiments/extract-fa-fix branch from 9421558 to ed076bc Compare January 30, 2025 19:37
@hovind
Copy link
Contributor Author

hovind commented Jan 30, 2025

I had made the mistake of adding related but ultimately independent changes to this PR. I have now updated the pull request to only include the minimal required changes. If anyone could have a look it would be greatly appreciated.

@oharboe
Copy link

oharboe commented Feb 6, 2025

@povik Thoughts?

@povik
Copy link
Member

povik commented Feb 6, 2025

@povik Thoughts?

I think I hope we will be able to obsolete this code soon in favor of something more readable.

if (func3.at(key).count(xor3_func)) {
SigBit YY = invert_xy ? module->NotGate(NEW_ID, Y) : Y;
SigBit YY = invert_xy ^ invert_y ? module->NotGate(NEW_ID, Y) : Y;
Copy link
Member

@povik povik Feb 6, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This makes sense: at this point we are looking to implement xor3, respectively xnor3 in terms of the signals held in A, B, C.

Y is the Y output of a (possibly cached) full-adder cell over A, B, C, with inversions inserted as indicated by f3i.inv_a/b/c, with the added caveat that if invert_xy is true, all of the inputs are complemented on top of that.

With that being said the logic around here seems correct to decide whether we need to use Y, or Y complemented to get the xor3/xnor3 result.

@povik povik merged commit 772b9c0 into YosysHQ:main Feb 6, 2025
25 checks passed
@povik
Copy link
Member

povik commented Feb 6, 2025

Thanks for the fix and for the included test case.

@whitequark
Copy link
Member

I have a better idea for fixing this pass: it's called rm. It's not useful!

@povik
Copy link
Member

povik commented Feb 6, 2025

I have a better idea for fixing this pass: it's called rm. It's not useful!

Our ideas are actually one and the same since what I hope will happen is that we will be able to move this reponsibility into a generic cell mapper. I am not sure what you mean about this pass not being useful since there happen to be plenty users using it to map to standard cells, and saving area/wiring in the process.

@whitequark
Copy link
Member

I am not sure what you mean about this pass not being useful since there happen to be plenty users using it to map to standard cells, and saving area/wiring in the process.

It's solving a subgraph logic equivalence problem, which isn't a great one to find yourself solving. If you are finding yourself solving it you should fix your flow so that it doesn't lower your adders down to gates first, not to do this.

@povik
Copy link
Member

povik commented Feb 6, 2025

I disagree it's so clear-cut, the cell mapper essentially does the same job for all other cells, it only needs to be extended slightly to handle this multi-output case.

@hovind
Copy link
Contributor Author

hovind commented Feb 7, 2025

Thanks for the fix and for the included test case.

Thanks for reviewing and pushing the change forward!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants